fifo+send(${\it es}$;$C$;${\it in}$;$m$;${\it req}$;$j$;$i$;$e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$($\uparrow$isrcv($e$)) \& lnk($e$) = ${\it in}$($j$) \& ((tag($e$) = $m$) $\vee$ (tag($e$) = ${\it req}$)) \& ($i$ $\in$ val($e$).1)